(* Final Exam --- December 27, 2021  
You are allowed to search and use any property provided in the 
standard library of Coq. *)

Require Import Nat.
Require Import List.
From LF Require Export Induction.

Notation "[ ]" := nil. 
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).


Definition admit {T: Type} : T.  Admitted.

(* 1. Prove the following fact about natural numbers. *)

Lemma mul_2_r : forall  n : nat, 
  (n + 1) * 2 = n + n + 2.
Proof.
  intros.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. rewrite plus_n_Sm. rewrite plus_n_Sm. rewrite plus_n_Sm.
    assert (S n = n+1).
    { destruct n. { reflexivity. }
      { simpl. rewrite <- plus_n_Sm. rewrite <- plus_n_O. reflexivity. }
    }
    rewrite H. rewrite add_assoc. simpl.
    symmetry. rewrite <- add_assoc. simpl. reflexivity.
Qed.

(* 2. Define a function called squared so that (squared n) returns true 
iff n is a squared number, i.e. n = n' * n' for some n'. *)

Fixpoint mySquare (n:nat)(o:nat):bool :=
  match o with
  | 0 => true
  | 1 => true
  | _ => match n with
          | 0 => false
          | S n' => if n'*n' =? o then true
                    else mySquare n' o
  end
end.

Definition squared (n : nat) : bool :=
  mySquare n n.

Example square_test1 : squared 8 = false.
Proof. reflexivity. Qed.

Example square_test2 : squared 25 = true.
Proof. reflexivity. Qed.


(* 3. Let two sequences of numbers F1(n) and F2(n) be given as follows.
   F1(0) = 0
   F1(n) = F1(n-1) + 2 * n   for n > 0.

   F2(0) = F2(1) = 1
   F2(n+2) = F2(n) + F2(n+1)    for n >= 0.

Define the function Seq such that (Seq n) returns the sequence

[F1(0); F2(0); F1(1); F2(1); ... ; F1(n); F2(n)].
*)

Fixpoint F1 (n:nat):nat :=
  match n with
  | 0 => 0
  | S n' => 2*n + (F1 n')
end.
Fixpoint F2 (n:nat):nat :=
  match n with
  | 0 => 1
  | 1 => 1
  | S n' => (F2 n')+(F2 (n'-1))
end.

Fixpoint Seq (n: nat) : list nat :=
  match n with
  | 0 => [F1 0;F2 0]
  | S n' => (Seq n') ++ [F1 n;F2 n]
end.

Example Seq_test :  Seq 5 = [0; 1; 2; 1; 6; 2; 12; 3; 20; 5; 30; 8].
Proof. reflexivity. Qed.


(* 4. Let oddn be the predicate that tests whether a given number
is odd or not. Show that the multiplication of two odd numbers is odd. *)

Inductive oddn : nat -> Prop :=
 | odd1 : oddn 1
 | odd2 : forall n, oddn n -> oddn (S (S n)).

Theorem odd_mul : forall n m, oddn n -> oddn m -> oddn (n * m).
Proof.
  induction n. intros.
  - simpl. apply H.
  - simpl. intros. Abort. (**rewrite add_assoc.
  induction m.
  + intros. simpl. rewrite<- mult_n_O. apply H0.
  + intros. simpl. destruct m.
    * simpl. Abort. rewrite mult_1_r. apply H0.
    * simpl. inversion H.
      * simpl. rewrite add_0_r. apply H0.
      * simpl. auto. Abort.*)


(* 5. Write a function (partition):

      partition : list nat -> list (list nat )

   which partitions a list into a list of 3 sublists. The first sublist
   contains all odd numbers divisible by 3 in the original list. 
   The second sublist contains all other odd numbers in the original list. 
   The last sublist contains all the even numbers in the original list. 
   The order of elements in the three sublists should be the same as their 
   order in the original list. 

   Hint: You may use the Coq function (filter).
*)

Fixpoint _3D (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S O)    => false
  | S (S (S n')) => _3D n'
  end.

Fixpoint partition3DOdd (l:list nat):list nat :=
  match l with
  | nil => nil
  | h::t => if _3D h && odd h then h::(partition3DOdd t)
            else partition3DOdd t
end.

Compute partition3DOdd [1;2;3;4;5;6;7;8;9;6;3].

Fixpoint partitionOdd (l:list nat):list nat :=
  match l with
  | nil => nil
  | h::t => if odd h && negb(_3D h) then h::(partitionOdd t)
            else partitionOdd t
end.

Compute partitionOdd [1;2;3;4;5;6;7;8;9;6;3].

Fixpoint partitionEven (l:list nat):list nat :=
  match l with
  | nil => nil
  | h::t => if even h then h::(partitionEven t)
            else partitionEven t
end.
Compute partitionEven [1;2;3;4;5;6;7;8;9;6;3].

Definition partition (l : list nat) : list (list nat) :=
  [partition3DOdd l; partitionOdd l; partitionEven l].

Example partition_test: 
  partition [1;2;3;9;4;5;6;15;8] = [[3; 9; 15]; [1; 5]; [2; 4; 6; 8]].
Proof. reflexivity. Qed.


(* 6. We call a natural number good if the sum of all 
   its digits is divisible by 5. For example 122 is good 
   but 93 is not. Define a function count such that 
   (count n) returns the number of good numbers smaller than 
   or equal to n. Here we assume that 0 <= n < 10000. 
   Hint: You may find the "let ... in" struct useful. You may 
   directly use the div and modulo functions defined in the 
   standard library of Coq. *)

Definition getSum (n:nat):nat :=
  n mod 10 + n / 10 mod 10 + n / 100 mod 100 + n / 1000 mod 1000.

Compute getSum 322.

Fixpoint count (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => if getSum(n) mod 5 =? 0 then 1+count(n')
            else count n'
end.

Example count_test1 : count 15 = 3.
Proof. reflexivity. Qed.

Example count_test2 : count 2005 = 401.
Proof. reflexivity. Qed.


(* 7. Prove the following fact about excluded middle. *)

Theorem double_neg : forall P : Prop,
  P -> ~~P.
Proof.
  intros P H. unfold not. intros G. apply G. apply H.  Qed.

Theorem de_morgan : 
   (forall P, P \/ ~P) -> (forall P Q, ~(~P /\ ~Q) -> P \/Q).
Proof.
  intros a b c d.
  assert (~b/\~c -> ~(b\/c)). {
    intros NANB AB.
    case AB.
    - intro A1.
      case NANB.
      intros NA NB.
      apply NA.
      exact A1.
    - intro B1.
      case NANB.
      intros NA NB.
      apply NB.
      exact B1.
  }
Abort.

(* 8. Consider the following type:

Inductive btree : Set :=
 | leaf : nat -> btree 
 | node : nat -> btree -> btree -> btree.
 
Define a function to give a preorder traversal of the tree and collect
all the odd numbers in a list. 
*)

Inductive btree : Set :=
 | leaf : nat -> btree 
 | node : nat -> btree -> btree -> btree.

Fixpoint preorder (t: btree) : list nat :=
  match t with
  | leaf n' => nil
  | node n' t1 t2 => (n'::(preorder t1))++(preorder t2)
end.

Example bt_test : preorder (node 5 (node 1 (leaf 0) (node 3 (leaf 2) (leaf 4))) 
                                   (node 9 (node 7 (leaf 6) (leaf 8)) (leaf 10))) 
                   = [5; 1; 3; 9; 7].
Proof. reflexivity. Qed.

(* 9. Write in Coq a function that swaps the maximum and minimum
elements in a list while keeping other elements unchanged. Suppose
all the elements in the input list are distinct and they range from 1 to 100.
*)

Fixpoint findMax l :=
  match l with
  | nil => 0
  | h::t => max h (findMax t)
end.

Fixpoint findMin l :=
  match l with
  | nil => 101
  | h::t => min h (findMin t)
end.

Compute findMax [1;4;5;6;7;3].
Compute findMin [1;4;5;6;7;3].

Fixpoint mySwap (l:list nat)(maxn:nat)(minn:nat) : list nat :=
  match l with
  | nil => nil
  | h::t => if h =? maxn then minn::(mySwap(t)(maxn)(minn))
            else if h =? minn then maxn::(mySwap t maxn minn)
            else h::(mySwap t maxn minn)
end.

Definition swap (l : list nat) : list nat :=
  mySwap(l)(findMax(l))(findMin(l)).

Example swap_test : swap [3;7;2;5;1;4;6] = [3;1;2;5;7;4;6].
Proof. reflexivity. Qed.


(* 10. The following definitions specify the abstract syntax of
    some arithmetic expressions and an evaluation function. *)

Inductive aexp : Type :=
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult a1 a2 => (aeval a1) * (aeval a2)
  end.

(* Suppose we define a function that takes an arithmetic expression 
   and slightly simplifies it, changing every occurrence of [e + 0],
   [e - 0] or [e * 1] into [e], and [e * 0] into [0]. *)

Fixpoint optimize (a:aexp) : aexp :=
  (* FILL IN HERE *) admit.

(* Prove the following theorem that states the correctness of the 
optimization with respect to the evaluation of arithmetic expressions. *)

Theorem optimize_mult1_sound: forall a,
  aeval (optimize a) = aeval a.
Proof. (* FILL IN HERE *) Admitted.
 
